FDL - Step of Proof: multiply_nat

Step of Proof: multiply_nat_wf

12,41

Inference at *
Iof proof for Lemma multiply nat wf:

i, j:

. (i * j)

by ((((UnivCD)

CollapseTHENA ((Auto_aux (first_nat 1:n) ((first_nat 1:n),(first_nat 3:n

C)) (first_tok :t) inil_term)))

)

CollapseTHEN (((MemTypeCD)

CollapseTHENA (

C(Auto_aux (first_nat 1:n) ((first_nat 1:n),(first_nat 3:n)) (first_tok :t) inil_term)))

))

C1:

C1: 1. i :

C1: 2. j :

C1:

(i * j)

C2: .....set predicate..... NILNIL

C2: 1. i :

C2: 2. j :

C2:

(i * j)

Definitions t T, , x:A. B(x),

Lemmas nat wf, le wf